IsMaxIdeal(r;m) == u:|r|. ((m(u)))  (v:|r|. (m((u * v) +r (-r(1))))) 

latex

---

clarification:

IsMaxIdeal(r;m) == u:|r|. ((m(u)))  (v:|r|. (m((u (*r) v) +r (-r(1r))))) 

latex

Up	rings 1
Wellformedness Lemmas	max ideal p wf
Definitions	x:A. B(x), P  Q, A, x:A. B(x), |r|, +r, x f y, *, -r, 1